//
//  cmsat.cpp
//  ltlbmc
//
//  Created by GD Huang on 7/9/12.
//  Copyright (c) 2012 __MyCompanyName__. All rights reserved.
//
#ifdef CMSAT_SOLVER
#include <iostream>
#include "Solver.h"

#define pos(var)  (var<<1)
#define neg(var)  ((var<<1)^1)

#define Manager void*

using namespace CMSat;

int TT, FF;
vec<Lit> ToCl_lits;
inline void ToCl(int* clause_lits,
                 int num_lits) {
    int i;
    
    ToCl_lits.clear();
    for(i=0; i<num_lits; i++)
        ToCl_lits.push(Lit::toLit(clause_lits[i]));
    
}



/***********************************************************
 Constructor/DestructorStatusT
 ***********************************************************/
//int FF, TT;

// init a manager  Solver * solver = (Solver*) mng;
Manager InitManager() {
    
    SolverConf conf;
    conf.verbosity = 2;
    Solver * solver = new Solver(conf);
    
    //FF & TT
    FF=solver->newVar(false);
    TT = solver->newVar(false);  
    return (Manager)solver;
    
}

// release a manager
void ReleaseManager(Manager mng) {
    Solver * solver = (Solver*) mng;
    delete solver;
}



/***********************************************************
 Problem specification
 ***********************************************************/
// add a variable
int NewVar(Manager mng, bool dvar) {
    Solver * solver = (Solver*) mng;
    return solver->newVar(dvar);
}

// Declare if a variable should be eligible for selection in the decision heuristic.
void SetDecisionVar(Manager mng, int var, bool b) {
    Solver * solver = (Solver*) mng;
    solver->setDecisionVar(var, b);
}

// add a clause
void AddClause(Manager mng, int num_lits, int* clause_lits) {
    
    Solver * solver = (Solver*) mng;
    ToCl(clause_lits, num_lits);
    solver->addClause(ToCl_lits);
}



vec<Lit> Assumption_lits;
void BeginAssumption(Manager mng) {
    Assumption_lits.clear();
}

void EndAssumption(Manager mng) {
}

void Assume(Manager mng, int o) {
    Assumption_lits.push(Lit::toLit(pos(o)));
}

void AssumeNot(Manager mng, int o) {
    Assumption_lits.push(Lit::toLit(neg(o)));
}

/***********************************************************
 Solving
 #define sTRUE 1
 #define sFALSE 0
 #define sUNDEF -1
 ***********************************************************/
//solve
int Solve(Manager mng) {
    Solver * solver = (Solver*) mng;
    Assume(mng, TT);
    AssumeNot(mng, FF);
    
    //solver->simplify();
    lbool result = solver->solve(Assumption_lits);
    return (result==l_True);
}

int Value(Manager mng, int var) {
    Solver * solver = (Solver*) mng;
    lbool result = solver->value(var);
    
    if(result==l_True)
        return 1;
    else if(result==l_False)
        return 0;
    else if(result==l_Undef)
        return -1;
    else
        assert(0 && "minisat_wrapper.c: GetVar(): unknown result");	
    
}



/***********************************************************
 Read state
 ***********************************************************/
// The current number of original clauses.
int NumClauses(Manager mng) {
    Solver * solver = (Solver*) mng;
    return solver->nClauses();
}

// The current number of variables.
int NumVars(Manager mng) {
    Solver * solver = (Solver*) mng;
    return solver->nVars();
}


#endif


